A method of using a set of a precondition and a postcondition of a program is known as a basic method of indicating specifications and properties of the program in an imperative programming language. An example of a known background theory includes axiomatic semantics that indicates validity of the program by delivering the precondition and the postcondition of the program through an axiom and an inference rule. Hoare logic is known as a specific example of the axiomatic semantics.
JP-A 2005-182806 (Kokai) describes a method of generating a program that satisfies a given specification and therein, a method using the axiomatic semantics is shown as a method example of describing a specification.